We identify two limitations of the verification approach.

% \emph{\bf{Semi-formal nature of the applied verification approach:}}
% While the verification approach is substantially rigorous, we have no proof that
% the translation from ATL transformations and their constrained metamodels to
% OCL and relational logic does not conflict with the semantics of ATL. This is
% due to the lack of complete formal semantics for ATL and OCL. Thus, the
% correctness of the used approach is only validated using semi-formal
% descriptions of ATL and OCL and using extensive testing. Thus, the used
% verification approach is currently not applicable to critical systems.
\emph{\bf{Correctness of ATL-to-relational-logic translation:}} % not proven:}}
Extensive testing and inspection was used to ensure that all steps involved in
the translation of ATL and OCL to first-order relational logic are correct.
However, in the absence of a formal semantics of ATL and OCL, a formal
correctness proof is impossible and the possibility of a bug in the translation
remains. This should be taken into account before our approach is used in the
context of safety-critical systems.

\emph{\bf{Bounded search approach:}} All verification approaches based on a
bounded search space cannot guarantee correctness of a transformation because
the scopes experimented with may have been too small. 
% This means that such approaches are not suitable to detect bugs that cannot be
% reproduced with small counterexamples. 
The maximum scope sufficient to show bugs in a transformation is
transformation-dependent. For example, a transformation with a multiplicity
invariant that requires a multiplicity to be 10, will require a scope of 11 to
generate a counterexample for that invariant, if any. 
% We do not have similar constraints in our transformation and thus, we are
% confident that a scope of 5 is sufficient to uncover any bugs. To assess the
% performance of the used approach, we experiment with scopes up to 12. 
With respect to our case study, we are confident that a scope of 5 is sufficient
to detect violations of the given constraints; we ran analyses with scopes up to
12, because we wanted to study the performance of the approach. Real proofs of
unsatisfiability can be created using SMT solvers and quantifier
reasoning~\cite{Buettner2012MoDELS}, but the problem is generally undecidable
(i.e., the SAT solver does not terminate on all transformations), and the
mapping presented in~\cite{Buettner2012MoDELS} does not yet cover all language
features used in our case study. Further, we have not yet applied any a priori
optimizations of the search problem, e.g., metamodel pruning~\cite{Sen2009b},
which we plan to apply for future work.
% bounded search space (e.g. our used approach) suffer from
% exponential explosion of the constraint solving times with
% increasing scopes. This means that such approaches are not suitable to detect
% bugs that cannot be reproduced with small counterexamples. Real proofs of unsatisfiability can be created using SMT
% solvers and quantifier reasoning~\cite{Buettner2012MoDELS}, but the problem is
% generally undecidable (i.e., the SAT solver does not terminate on all
% transformations), and the mapping presented in~\cite{Buettner2012MoDELS} does not yet cover all
% language features used in our case study. Further, we have not yet applied any
% a priori optimizations of the search problem, e.g. metamodel
% pruning~\cite{Sen2009b}, which we plan to apply for future work. The
% maximum scope sufficient to show bugs in a transformation is transformation-dependent.
% For example, a transformation with a multiplicity invariant that requires a
% multiplicity to be 10, will require a scope of 11 to generate
% a counterexample for that invariant, if any. We do not have similar constraints
% in our transformation and thus, we are confident that a scope of 5 is sufficient
% to uncover any bugs. To assess the performance of the used approach, we experiment
% with scopes ranging from 4 to 12.
% Thus, without assigning specific upper bounds for
% individual types, the approach is limited to comparably small class extents.
%
% \emph{\bf{The nature of our GM-to-AUTOSAR transformation:}} Our case study
% explored a transformation that manipulates metamodels that are considered large
% on an industrial scale. The transformation, although far from being trivial,
% does not fully manipulate the two metamodels. We conducted a couple of
% experiments that show that the verification problem scales almost linearly when
% more independent rules are added. However, we still need to investigate the
% performance on larger and more complex transformations.
%%% Local Variables:
%%% TeX-master: "master"
%%% End: